Nuprl Lemma : choicef_wf
9,38
postcript
pdf
xm
:XM,
T
:Type,
P
:(
T
). (
a
:
T
.
P
(
a
))
((
x
:
T
.
P
(
x
))
T
)
latex
ProofTree
Definitions
x
:
T
.
P
(
x
)
,
t
T
,
x
(
s
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
,
x
:
A
.
B
(
x
)
,
P
Q
,
Dec(
P
)
,
XM
,
False
,
A
Lemmas
xmiddle
wf
,
not
wf
origin
xm:XM, T:Type, P:(T
). (
a:T. P(a)) 
((
x:T. P(x)) T)
xm:XM, T:Type, P:(T). (a:T. P(a)) ((x:T. P(x)) T)
x:T. P(x) Tx:A. B(x) Qx:A. B(x)
Q
A